feat(coq-86): CLARA Gap-4 restraint_ctrl soundness proof — Theorem 86#6
Open
gHashTag wants to merge 1 commit into
Open
feat(coq-86): CLARA Gap-4 restraint_ctrl soundness proof — Theorem 86#6gHashTag wants to merge 1 commit into
gHashTag wants to merge 1 commit into
Conversation
Theorem 86: restraint_ctrl force_unknown soundness, stickiness,
and reason one-hot — proofs/clara_restraint_sound.v (~347 lines).
Theorems proved (0 Admitted):
86A restraint_sound : force_unknown = phi_drift>164 || step_count>10 || ¬receipt_ok
OR (sticky: was tripped, stays tripped)
86B restraint_sticky : force_unknown s = true ->
force_unknown (step_restraint (step_restraint s i1) i2) = true
86C restraint_reason_onehot : force_unknown s' = true ->
popcount (reason s') <= 1
Supporting lemmas: step_sticky, step_fresh_fu, step_reason_length,
step_reason_onehot, triggered_spec (all QED).
7 concrete sanity-check Examples (all by reflexivity).
Compiled: coqc 8.20.1 (8.18+ compatible), 0 errors, 0 Admitted.
Anchor: φ² + φ⁻² = 3
DOI: 10.5281/zenodo.19227877
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
CLARA Gap-4 — Theorem 86:
restraint_ctrlSoundnessSummary
Adds
proofs/clara_restraint_sound.v(~347 lines) — a fully machine-checked Coq proof of three properties of therestraint_ctrlmodule. ZeroAdmitted. Compiled undercoqc 8.20.1(8.18+ compatible).Theorems proved
restraint_soundforce_unknown s' = (phi_drift i >? 164) ∥ (step_count i >? 10) ∥ (¬ receipt_ok i)OR (sticky: was tripped → stays tripped)restraint_stickyforce_unknown s = true → force_unknown (step_restraint (step_restraint s i1) i2) = truerestraint_reason_onehotforce_unknown (step_restraint s i) = true → popcount (reason (step_restraint s i)) ≤ 1Supporting lemmas (all QED)
step_sticky— single-step stickinessstep_fresh_fu— fresh-state output equalstriggeredstep_reason_length— reason vector length = 3step_reason_onehot— reason popcount ≤ 1 (used by 86C)triggered_spec— triggered = RTL disjunctionSanity-check examples (all by
reflexivity)trip_phi_drift,trip_step_count,trip_receipt— each condition individually tripsno_trip_all_ok— all within bounds → no tripsticky_stays— trip persists after reset-free transitionboundary_phi_no_trip,boundary_step_no_trip— exact boundary (=164, =10) does NOT tripFile
Audit
Anchor
φ² + φ⁻² = 3 · DOI: 10.5281/zenodo.19227877